COMMENT ⊗   VALID 00015 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00003 00002	.TURN ON "{#%α\"
C00005 00003	.NEXT PAGE
C00008 00004	Programs written with %5lit%1 in this way have a number of advantages.
C00010 00005	%7Some examples illustrating the power of lit%1
C00012 00006	(4)\If %5complement[xy]%1 is a list representing the complement of
C00015 00007	
C00018 00008	In order to state the first property let %5maxl[x]%1 be the maximum of the
C00021 00009	Then %5flatten%1 isn't %5lit%1-computable. For if it were then by theorem 1 there 
C00024 00010	
C00027 00011	
C00030 00012	To see that this implies that %5rev%1 isn't  %5mapcar%1-computable
C00032 00013	Note that this makes sence even if %5f%1 takes more than one argument
C00035 00014	
C00036 00015	
C00037 ENDMK
C⊗;
.TURN ON "{#%α\"
.TURN OFF "-" 

.DEVICE XGP;


.HLINES← IF XCRIBL THEN 53 ELSE 53;	<< NUMBER OF LINES/PAGE >>
.WCHARS← IF XCRIBL THEN 81 ELSE 69;	<< NUMBER OF CHARS/LINE >>
.PAGE FRAME HLINES+2 HIGH WCHARS WIDE;
.AREA TEXTER LINES 4 TO HLINES CHARS 1 TO WCHARS;
.TITLE AREA FOOTING LINE HLINES+1 CHARS 1 TO WCHARS;
.TITLE AREA HEADING LINES 1 TO 3 CHARS 1 TO WCHARS;
.PLACE TEXTER;


.COUNT FOOTNOTE INLINE TO 4 IN PAGE PRINTING "%3*1%*";

.AT "⊗↓" ENTRY "←" ⊂NEXT FOOTNOTE ; ! ;
.XGENLINES←XGENLINES-1;
.SEND FOOT ⊂
{!} ENTRY
.BREAK ⊃ ⊃

.FOOTSEP ← "_______" ;

.FONT 5 "CTL25";
.FONT 2 "GRK30";
.FONT 3 "SUP";
.FONT 4 "SUB";
.FONT 1 "LPT";
.FONT 6 "LPT"
.FONT A "NGB30"
.FONT 7 "XMAS40"



.AT "|" N "|"  ⊂
%4{}N{}%*{⊃

.MACRO e(n) ⊂"=|(n)|"⊃



.PORTION MAINPORTION
.COMPACT
.COUNT PAGE TO 999;
.COUNT FOOTNOTE INLINE TO 4 IN PAGE PRINTING ⊂"*"⊃;
 

.NEXT PAGE
.TURN ON "{","}","%";
.FILL
.begin center;select 1;
%7LIT%1
.end
%7Introduction%1

If x,y are LISP S-expressions and f is a binary operation on S-expressions
then define ⊗↓All definitions are written in LISP M-expression notation%3[2]%1←
%5lit[x;y;f]%1 by:
.begin center;
.select 5;

lit[x;y;f]=[null[x]→y;f[car[x];lit[cdr[x];y;f]]]
.end
Thus %5lit[(x|1|...x|n|);x|n+1|;f]=f[x|1|;f[x|2|;...;f[x|n|;x|n+1|]...]].
lit%1 was invented by Barron and Strachey%3[1]%1as a generalization of the
%2S%1 and %2P%1 notations for iterated sums and products i.e.

.begin center;select 5;
%2S%3n+1%4i=1%5x|i| = lit[(x|1|...x|n|);x|n+1|;plus]
.end
.begin center;select 5;
%2P%3n+1%4i=1%5x|i| = lit[(x|1|...x|n|);x|n+1|;times]
.end
Using it, and without any other recursion (that is except that impllcit
in the definition of %5lit%1) it's possible to write elegant programs
for computing many simple functions. For example the concatenating function
%5append%1 is given by:

.begin center; select 5;
append[x;y]=lit[x;y;cons]
.end

.begin nofill;select 5;
%1Thus:%5
     append[(x|1|...x|n|);(y|1|...y|m|)]=lit[(x|1|...x|n|);(y|1|...y|m|);cons]
                                        =cons[x|1|;...;cons[x|n|;(y|1|...y|m|)]...]      
                                        =(x|1|...x|n|y|1|...y|m|)
.end
Similarly the reversing function %5rev%1 may be defined by:

.begin;nofill;select 5;
   rev[x]=lit[x;NIL;λ[[y|1|;y|2|];append[y|2|;(y|1|)]]]
         =lit[x;NIL:λ[[y|1|;y|2|];lit[y|2|;cons[y|1|;NIL];cons]]]
.end
so e.g. %5rev[(1 2 3)]=(3 2 1)%1




Programs written with %5lit%1 in this way have a number of advantages.
Firstly as %5lit%1 can be efficiently coded iteratively it's possible to
optimize all such programs by using the iterative code to eliminate the
stacking overheads implicit in recursion. Secondly proofs of properties of
such programs can somtimes be got (without the need for induction) by
exploiting algebraic properties of %5lit%1. For example the associativity
of %5append%1 is a simple instance of:

.begin; center;select 5;
∀xyzf.  lit[append[x;y];z;f]=lit[x;lit[y;z;f];f]
.end
So induction need only be used to establish the general fact above and
this has uses besides showing %5append%1 is associative. Thus both the task of
efficiently compiling programs and the task of verifying them are simplified if
%5lit%1, rather than arbitrary recursion, is used.

In what follows I describe some facts which illucidate just which functions
can and which can't be computed by using %5lit%1 as above.

%7Some examples illustrating the power of lit%1

If a set (of integers) is represented by a list of it's members then many of the
operations of boolean algebra can be written with with %5lit%1. For example:
.tabs 5;

(1) If %5member[x;y]%1 is %5T%1 if %5x%1 is a member of (the set computed by)
%5y%1 and %5F%1 otherwise then:
.begin nofill;select 5;

member[x;y]=lit[y;F;λ[[z|1|;z|2|];[eq[T;z|3|]→T;
                                   eq[z|1|;x]→T;
                                            T→F]]]

.end
\e.g.%5 member[2;(1 2 3)]=T, member[2;(1 4 3)]=F%1

(2)\If %5union[x;y]%1 is a list representing the union of (the sets represented
by) %5y%1 and %5F%1 otherwise then:
.begin nofill;select 5;

        union[x;y]=lit[x;y;λ[[z|1|;z|2|];[member[z|1|;y]→z|2|;
                                                       T→cons[z|1|;z|2|]]]]
.end
\e.g.%5union[(1 2 3);(2 4 3)]=(1 3 2 4 5)%1

(3)\If %5intersection[x;y]%1 is a list representing the union of (the sets
represented by) %5x%1 and %5y%1, then:
.begin nofill;select 5;

        intersection[x;y]=lit[x;NIL;λ[[z|1|;z|2|];[member[z|1|;y]→cons[z|1|;z|2|];
                                                               T→z|2|]]]
.end;
\e.g %5intersection[(1 2 3);(1 3 4)]=(1 3)%1





(4)\If %5complement[x;y]%1 is a list representing the complement of
(the set represented by) %5x%1 in (the set represented by) %5y%1, then:
.begin nofill;select 5;

        complement[x;y]=lit[y;NIL;λ[[z|1|;z|2|];[member[z|1|;x]→z|2|;
                                                              T→cons[z|1|;z|2|]]]]
.end
\e.g. %5complement[(1 3);(1 2 3)]=(2)%1

(5)\If %5boolean[x]%1 is a set representing the set of all subsets of x then:
.begin nofill;select 5;

        boolean[x]=lit[x;cons[NIL;NIL];
                       λ[[y|1|;y|2|];
                         lit[y|2|;y|2|;
                             λ[[z|1|;z|2|];
                               append[z|2|;cons[cons[y|1|;z|1|];NIL]]]]]]
.end
\e.g. %5boolean[(1 2 3)]=( NIL (3) (2 3) (2) (1 2) (1 2 3) (1 3) (1) )%1
.begin nofill;
\(%5boolean%1 is due to Dave DuFeu)
.end
(6)\If lists %5x|1|,...,x|n|%1 represent sets S|1|,...,S|n|
respectively and %5cartprod[(x|1|...x|n|)]%1 represents S|1|x...xS|n| then:
.begin nofill;select 5;

        cartprod[x]=lit[x;cons[NIL;NIL];
                        λ[[y|1|;y|2|];
                          lit[y|1|;NIL;
                              λ[[z|1|;z|2|];
                                lit[y|2|;z|2|;
                                    λ[[w|1|;w|2|];
                                      cons[cons[z|1|;w|1|];w|2|]]]]]]]

    e.g.cartprod[( (1 2) (3 4) )]=( (1 3) (1 4) (2 3) (2 4) )

          cartprod[( (1 2) (3 4) (5 6) )]=( (1 3 5) (1 3 6) (1 4 5) (1 4 6) 
                                         =  (2 3 5) (2 3 6) (2 4 5) (2 4 6) )
.end
.begin nofill;
\(%5cartprod%1 is due to C. Strachey)
.end





%7Some results on the limitations of lit%1

To investigate which functions are not computable with %5lit%1 it's
necessary to define rigorously a notion of "%5lit%1-computability"
which formalizes the way of using %5lit%1 illustrated intuitively above.
There seem to be two natural ways of doing this: one could define the
class of %5lit%1-computable functions as the smallest class containing
certain basic functions (such as %5car,cdr,cons,atom,eq,null,cond%1) which is
closed under certain composition rules (e.g. if %5f%1 is in the class then
so is %5λ[[x;y];lit[x;y;f]]%1). Alternatively one could set up the (syntax
and semantics of ) a programming language whose programs were function
definitions like those above, then a function would be %5lit%1-computable
if and only if there exists a program which computes it.
As the latter method corresponds more directly to the intuitive idea I'm trying
to capture I use it. Having defined rigorously what it is for a function to
be %5lit%1-computable one can then try and find properties that all such 
functions must have. Then to show that a functionis not %5lit%1-computable
it suffices to show that it lacks one of the properties.

I shall now describe two properties possesed by all %5lit%1-computable
functions, both these relate the complexity (in an intuitive sense) of the 
functions values to that of it's arguments. 


In order to state the first property let %5maxl[x]%1 be the maximum of the
length of %5x%1 and the lengths of all 'sublists` of %5x%1. Rigorously
define %5maxl%1 recursively by:
.begin nofill;select 5;
                 0                               if x is an atom
    maxl[x]= 
                 maxα{maxl[x|1|],   ,maxl[x|n|]α} if x=(x|1|...x|n|)
.end
Also let N=α{0,1,2,...α}. The following theorem says that each %5lit%1-computable
function %5f%1 has the property that a bound on %5 maxl[f[x|1|;...;x|n|]]%1
can be computed from %5maxl[(x|1|...x|n|)]%1

Theorem 1

If %5f%1 is an n-argument %5lit%1-computable function (and n>0) then there
exists a function L|f|:N→N such that for all lists x|1|,...,x|n|:
.begin center;select 5;
maxl[f[x|1|;...;x|n|]]≤L|f|[maxl[(x|1|...x|n|)]]
.end
Proof
The theorem can be proved by strucural induction on the program which computes
%5f%1. L|f| can be found effectively from %5f%1 and is primitive recursive.

From theorem 1 it follows that if %5flatten%1 is the function which remouves 
all except the outermost brackets from a list i.e.if
.begin nofill;select 5;
    flatten[x]=[null[x]→NIL;
                atom[x]→cons[x;NIL];
                      T→append[flatten[car[x]];flatten[cdr[x]]]]

%1so e.g.%5 flatten[(1 (2 3 (4)) 5 6)]=(1 2 3 4 5 6).
.end

Then %5flatten%1 isn't %5lit%1-computable. For if it were then by theorem 1 there 
would be a function L|flatten|:N→N such that:
.begin center;select 5;
∀x. maxl[flatten[x]]≤L|flatten|[maxl[x]]
.end
But this is impossible for if for n≥1 x|n| is defined by:
.begin nofill;select 5;
      x|1|=(1)=cons[1;1]
    x|n+1|=(x|n|.x|n|)=cons[x|n|;x|n|]
.end
Then %5flatten[x|n|]=(1 1...1)%1 - a list of length 2%3n%1 - whilst for all n
%5maxl[x|n|]=2%1 so for large enough n we must have:
.begin center;select 5;
maxl[flatten[x|n|]]=2%3n%5>L|flatten|[2]=L|flatten|[maxl[x|n|]]
.end
which contradicts theorem 1.

The second property of %5lit%1-computable functions to be described implies
that %5equal%1 - the equality predicate on S-expressions - isn't 
%5lit%1-computable. To state this property I need to define for each n≥0 a
binary relation {e(n)} on S-expressions which is intuitively such that
%5x{e(n)}y%1 if and only if %5x%1 and %5y%1 (regarded as binary trees)
are the same up to depth n. More precisely:
.begin nofill;select 5;

      x{e(0)}y <=> x=y or (neither x nor y are atoms)

    x{e(n+1)}y <=> x=y or ( (neither x nor y are atoms) and
                            (car[x]{e(n)}car[y]) and (cdr[x]{e(n)}cdr[y]) )
.end
Theorem 2 below says that for each %5lit%1-computable function %5f%1
to make %5f[x|1|;...;x|n|] %1 agree with %5f[y|1|;...;y|n|]%1 to depth m it's 
sufficient to make each %5x|i|%1 agree with %5y|i|%1 up to depth m+k
where k is a constant which depends on%5f,maxl[(x|1|...x|n|)]%1
and %5maxl[(y|1|...y|n|)]%1 (and can be found effectively from these).
.next page;


Theorem 2

If %5f%1 is an n-argument %5lit%1-computable function (and n>0) then there
exists a function D|f|:NxN→N such that for all lists %5x|1|,...,x|n|,
y|1|,...,y|n|%1 if k=D|f|%5[maxl[(x|1|...x|n|)];maxl[(y|1|...y|n|)]]%1 then:
.begin center;select 5;
∀ m≥0. (x|1|{e(m+k)}y|1|,...,x|n|{e(m+k)}y|n|) => f[x|1|;...;x|n|]{e(m)}f[y|1|;...;y|n|]
.end

Proof
 As with theorem 1, theorem 2 can be proved by structural induction on
the program which computes %5f%1. D|f| can be effectively found from
%5f%1 and is primitive recursive.

To see how theorem 2 entails the non %5lit%1-computability of %5equal%1
suppose that it does apply to it so that there exists a function
D|equal|:NxN→N with the properties described above. Now for n≥0 define a|n|,
b|n| inductively by:
.begin nofill;select 5;
      a|0|=(1)=cons[1;NIL]            b|0|=(2)=cons[2;NIL]
    a|n+1|=(a|n|)=cons[a|n|;NIL]    b|n+1|=(b|n|)=cons[b|n|;NIL]
.end
Then for all n %5maxl[a|n|]=maxl[b|n|]=1%1 so in particular if 
k=D|equal|[1;1] then %5maxl[a|k|]=maxl[b|k|]=1%1 and so by theorem 2
(with m=0, n=2, %5x|1|=x|2|=y|1|=a|k|, y|k|=b|k|%1)
we should have
.begin center;select 5;
a|k|{e(k)}a|k|,a|k|{e(k)}b|k| => T=equal[a|k|;a|k|]{e(0)}equal[a|k|;b|k|]=F
.end
But this implication is false as it's antecedant (i.e.%5a|k|{e(k)}a|k| and
a|k|{e(k)}b|k|%1)  is true whilst it's consequent (i.e %5T{e(0)}F%1) isn't.








%7An alternative characterization of lit%1-%7computability%1

One might expext that the class of %5lit%1-computable functions is
rather arbitrary and dependant on the exact definition of %5lit%1, however 
it turns out that this isn't so. To illustrate this I'll sketch out a
completely different characterization of %5lit%1-computability based on
the use of %5mapcar%1 together with a stack (for temporary working space)
%5mapcar%1 is the LISP function defined by:
.begin center;select 5;
mapcar[x;f]=[null[x]→NIL;T→cons[f[car[x]];mapcar[cdr[x];f]]]
.end
Thus %5mapcar[(x|1|...x|n|);f]=(f[x|1|]...f[x|n|])%1 it can be written in terms of
%5lit%1 by:
.begin center;select 5;
mapcar[x;f]=lit[x;NIL;λ[[y|1|;y|2|];cons[f[y|1|];y|2|]]]
.end
but there are many functions which are %5lit%1-computable but can't
be expressed as an applicative expression built up from %5mapcar%1 and LISP
primatives (excluding %5label%1 - e.g.recursion). An example of such a function
is %5rev%1, to show this it's necessary to rigorously define a notion of
"%5mapcar%1-computable" analogous to "%5lit%1-computable" and then one
can  prove:
.next page;
Theorem 3

For each %5mapcar%1-computable function %5f%1 and each m≥0 there exists a
k≥0 such that:
.begin center;select 5;
x{e(k)}y => f[x]{e(m)}f[y]
.end

Proof

Similar (but much easier) to theorems 1 and 2

To see that this implies that %5rev%1 isn't  %5mapcar%1-computable
assume that it is and apply theorem 3 with m=1,%5x=(0...0 1),y=(0...0 1)%1
where %5x y%1 have lengths greater than k. Then x{e(k)}y but
not %5rev[x]=(1 0...0){e(1)}(2 0...0)=rev[y]%1 contradicting theorem 3.

What does one have to add to %5mapcar%1 to get the power of %5lit%1?
It turns out that if one allows programs to pop and push S-expressions
on to a stack during computations then this is sufficient. To make this
clearer let an expressionof the form "%5e;%1" where %5e%1 is a LISP form
mean "evaluate %5e%1 and push the result on to the stack" and if %5f%1 is
a LISP function let "%5.f;%1" mean "pop the appropriate number of
arguments from the stack, apply %5f%1 and push the result on to the stack".
Thus:
.begin center; select 5;
(1 2);.cons;
.end
means push (1 2) on the stack, then pop it, apply %5cons%1 and push the
result back on to the stack. In general
.begin center;select 5;
f[e|1|;...;e|n|];
.end
means the same as 
.begin center;select 5;
e|1|;...;e|n|;.f;
.end 
and
.begin center ;select 5;
mapcar[(x|1| x|2|...x|n|);f]
.end
means
.begin center;select 5;
x|1|;.f;x|2|;.f;...;x|n|;.f;
.end
Note that this makes sence even if %5f%1 takes more than one argument
e.g.
.begin center; select 5;
1;mapcar[(2);cons]≡1;2;.cons;≡cons[1;2];≡(1 2);
.end

With this notation one can now write %5lit%1 with %5mapcar%1 + stack
as follows:
.tabs 64;
.begin nofill;select 5;
    lit[x;y;f]=mapcar[x;λ[[z];z;NIL]];                            \-1-
               .λ[[z];y];                                         \-2-
               mapcar[x;λ[[z|1|;z|2|;z|3|];f[z|1|;z|2|];NIL]];    \-3-
               .λ[[z|1|;z|2|];z|1|];                              \-4-
.end
The end result of evaluating the right hand side of the above expression is to
push %5lit[x;y;f]%1 on the stack. This works as follows:
Suppose %5x=(x|1|...x|n|)%1 then the effect of line -1- is to push
%5x|1|,NIL,...,x|n|,NIL%1 on to the stack. Line -2- then replaces the top %5NIL%1
with %5y%1 and line -3- transforms the stack from
.next page;
.begin nofill;select 5;
    ......x|1|,NIL,...,x|n|,y
%1to%5
    ......x|1|,NIL,...,x|n-1|,NIL,f[x|n|;y]
%1then to%5
    ......x|1|,NIL,...,x|n-2|,NIL,f[x|n-1|;f[x|n-2|;y]]
%1and eventually to%5
    ......f[x|1|;...;f[x|n|;y]...],NIL
.end
Finally line -4- remouves the %5NIL%1 at the top of the stack to leave
%5f[x|1|;...;f[x|n|;y]...]=lit[(x|1|...x|n|);y;f]%1 as required.

%7Open problems%1

1:
So far I havn't found any functions which arn't %5lit%1-computable
but can't be shown to be so with theorems 1 and 2. I conjecture that a function
is %5lit%1-computable if and only if theorems 1 and 2 hold of it.

2:
A number of people have suggestedto me that an algebraic definition of
%5lit%1-computability could be given which would greatly increase the
elegance of the (at present rather contorted) proofs. Working out the details
is an open problem. Can %5mapcar%1-computability be studied algebraically? - 
it's much less clear to me how to do this than how to handle %5lit%1.

%7References%1

[1]:
Barron, D.W. and Strachey, C. "Programming" in Chapter 3 of "Advances in
Programming and Non-numerical Computation", edited by L.Fox,Pergamon Press
(1966).

[2]:
McCarthy, J. et al.,"LISP 1.5 Programmer's Manual",MIT Press (1969).